// $Id: CoveringTree.cs 101 2007-05-08 18:17:16Z karolina.zarawska $ 

using System;
using System.Collections.Generic;
using System.Text;
using System.IO;
using Base;
using Algorithms.Numerical;
using PetriDiagram.Algorithms;
using PetriDiagram.Model;
using PetriDiagram;

namespace Algorithms
{
    public class CoveringTree
    {
        private Vertex root = null;
        private StateSpaceAnalysis analysis;

        //List of covering markings:
        private List<MarkingVector> markings;
        private List<MarkingVector> oldMarkings;

        public CoveringTree()
        {
            analysis = new StateSpaceAnalysis();
            markings = new List<MarkingVector>();
            oldMarkings = new List<MarkingVector>();
        }

        public Vertex Build(IntMatrix incidentionMatrix, MarkingVector marking, 
            PetriNetModel model)
        {
            if (root != null) return root;
            return ReBuild(incidentionMatrix.Transponed, marking, model);

        }

        public Vertex ReBuild(IntMatrix incidentionMatrix, MarkingVector marking,
            PetriNetModel model)
        {
            if (marking.Length == 0)
            {
                throw new InvalidDataException("Empty incoming marking vector!");
            }

            if ((incidentionMatrix.Height == 0) || (incidentionMatrix.Width == 0))
            {
                throw new InvalidDataException("Empty incidention matrix!");
            }
            
            analysis.Reset();
            markings.Clear();
            markings.Add(marking);

            root = new Vertex(marking);
            List<Vertex> path = new List<Vertex>();
            path.Add(root);
            Build(root, path, incidentionMatrix, model);

            analysis.CheckBoundless(this.oldMarkings, this.markings);

            return root;
        }

        private void Build(Vertex vertex, List<Vertex> vertexPath, IntMatrix matrix,
            PetriNetModel model)
        {
            IntMatrix minusMatrix = this.MinusMatrix(matrix);

            Boolean deadEnd = true;

            Transition[] trans =  new Transition[model.Transitions.Count];
            model.Transitions.CopyTo(trans, 0);

            for (int i = 0; i < matrix.Height; i++)
            {
                
                if (vertex.Marking.canFire(minusMatrix.getRow(i))
                    && vertex.Marking.canFire(model.GetIncomingInhibitors(trans[i]), model))
                {
                    deadEnd = false;

                    Vertex child = new Vertex(vertex.Marking.add(matrix.getRow(i)));
                    child.Parent = vertex;
                    child.ComingTransition = i;

                    child.markOmega(vertexPath);

                    if (!child.checkForOldMarking(vertexPath))
                    {
                        if (!markings.Contains(child.Marking))
                            markings.Add(child.Marking);

                        vertexPath.Add(child);
                        Build(child, vertexPath, matrix, model);
                        vertexPath.Remove(child);
                    }
                    else
                    {
                        if (!oldMarkings.Contains(child.Marking))
                            oldMarkings.Add(child.Marking);
                    }

                    vertex.Children.Add(child);
                }
            }

            if (deadEnd)
            {
                vertex.Flag = Vertex.Flags.DeadEnd;
                this.analysis.Deadlock = true;
                this.analysis.CountPathToDeadlock(vertex);
            }
        }

        private IntMatrix MinusMatrix(IntMatrix matrix)
        {
            IntMatrix m = new IntMatrix(matrix.Height, matrix.Width);

            for (int x = 0; x < matrix.Height; x++)
                for (int y = 0; y < matrix.Width; y++)
                    m[x, y] = Math.Max(0, -matrix[x, y]);

            return m;
        }

        public Vertex Root
        {
            get { return root; }
        }

        public StateSpaceAnalysis Analysis
        {
            get { return analysis; }
        }
    }
}
